a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ DependencyPairsProof
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ QTRS
↳ DependencyPairsProof
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
B(b(d(d(b(b(x1)))))) → C(x1)
B(b(d(d(b(b(x1)))))) → A(c(c(x1)))
A(a(x1)) → B(b(x1))
A(a(d(d(x1)))) → B(x1)
A(a(d(d(x1)))) → B(b(x1))
A(a(x1)) → B(b(b(b(b(x1)))))
B(b(d(d(b(b(x1)))))) → A(a(c(c(x1))))
A(a(x1)) → B(b(b(x1)))
B(b(d(d(b(b(x1)))))) → C(c(x1))
A(a(x1)) → B(b(b(b(x1))))
A(a(x1)) → B(b(b(b(b(b(x1))))))
A(a(x1)) → B(x1)
a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
B(b(d(d(b(b(x1)))))) → C(x1)
B(b(d(d(b(b(x1)))))) → A(c(c(x1)))
A(a(x1)) → B(b(x1))
A(a(d(d(x1)))) → B(x1)
A(a(d(d(x1)))) → B(b(x1))
A(a(x1)) → B(b(b(b(b(x1)))))
B(b(d(d(b(b(x1)))))) → A(a(c(c(x1))))
A(a(x1)) → B(b(b(x1)))
B(b(d(d(b(b(x1)))))) → C(c(x1))
A(a(x1)) → B(b(b(b(x1))))
A(a(x1)) → B(b(b(b(b(b(x1))))))
A(a(x1)) → B(x1)
a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
B(b(d(d(b(b(x1)))))) → A(c(c(x1)))
A(a(x1)) → B(b(x1))
A(a(d(d(x1)))) → B(x1)
A(a(d(d(x1)))) → B(b(x1))
A(a(x1)) → B(b(b(b(b(x1)))))
A(a(x1)) → B(b(b(x1)))
B(b(d(d(b(b(x1)))))) → A(a(c(c(x1))))
A(a(x1)) → B(b(b(b(x1))))
A(a(x1)) → B(b(b(b(b(b(x1))))))
A(a(x1)) → B(x1)
a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
A(a(d(d(x1)))) → B(x1)
A(a(d(d(x1)))) → B(b(x1))
POL(A(x1)) = x1
POL(B(x1)) = x1
POL(a(x1)) = x1
POL(b(x1)) = x1
POL(c(x1)) = 1 + 2·x1
POL(d(x1)) = 1 + 2·x1
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
B(b(d(d(b(b(x1)))))) → A(c(c(x1)))
A(a(x1)) → B(b(x1))
A(a(x1)) → B(b(b(b(b(x1)))))
B(b(d(d(b(b(x1)))))) → A(a(c(c(x1))))
A(a(x1)) → B(b(b(x1)))
A(a(x1)) → B(b(b(b(x1))))
A(a(x1)) → B(b(b(b(b(b(x1))))))
A(a(x1)) → B(x1)
a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
B(b(d(d(b(b(x0)))))) → A(d(d(x0)))
B(b(d(d(b(b(c(x0))))))) → A(c(d(d(x0))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
A(a(x1)) → B(b(x1))
A(a(x1)) → B(b(b(b(b(x1)))))
A(a(x1)) → B(b(b(x1)))
B(b(d(d(b(b(x1)))))) → A(a(c(c(x1))))
B(b(d(d(b(b(x0)))))) → A(d(d(x0)))
A(a(x1)) → B(b(b(b(x1))))
B(b(d(d(b(b(c(x0))))))) → A(c(d(d(x0))))
A(a(x1)) → B(b(b(b(b(b(x1))))))
A(a(x1)) → B(x1)
a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
A(a(x1)) → B(b(x1))
A(a(x1)) → B(b(b(b(b(x1)))))
A(a(x1)) → B(b(b(x1)))
B(b(d(d(b(b(x1)))))) → A(a(c(c(x1))))
A(a(x1)) → B(b(b(b(x1))))
A(a(x1)) → B(b(b(b(b(b(x1))))))
A(a(x1)) → B(x1)
a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
A(a(x1)) → B(x1)
Used ordering: Polynomial interpretation [25]:
A(a(x1)) → B(b(x1))
A(a(x1)) → B(b(b(b(b(x1)))))
A(a(x1)) → B(b(b(x1)))
B(b(d(d(b(b(x1)))))) → A(a(c(c(x1))))
A(a(x1)) → B(b(b(b(x1))))
A(a(x1)) → B(b(b(b(b(b(x1))))))
POL(A(x1)) = 1 + 8·x1
POL(B(x1)) = x1
POL(a(x1)) = 1 + 8·x1
POL(b(x1)) = 9
POL(c(x1)) = 0
POL(d(x1)) = 0
c(c(x1)) → d(d(x1))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
a(a(d(d(x1)))) → d(d(b(b(x1))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
A(a(x1)) → B(b(x1))
A(a(x1)) → B(b(b(b(b(x1)))))
B(b(d(d(b(b(x1)))))) → A(a(c(c(x1))))
A(a(x1)) → B(b(b(x1)))
A(a(x1)) → B(b(b(b(x1))))
A(a(x1)) → B(b(b(b(b(b(x1))))))
a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
A(a(d(d(b(b(x0)))))) → B(b(b(a(a(c(c(x0)))))))
A(a(b(d(d(b(b(x0))))))) → B(b(b(b(a(a(c(c(x0))))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
A(a(x1)) → B(b(x1))
A(a(x1)) → B(b(b(x1)))
B(b(d(d(b(b(x1)))))) → A(a(c(c(x1))))
A(a(d(d(b(b(x0)))))) → B(b(b(a(a(c(c(x0)))))))
A(a(x1)) → B(b(b(b(x1))))
A(a(x1)) → B(b(b(b(b(b(x1))))))
A(a(b(d(d(b(b(x0))))))) → B(b(b(b(a(a(c(c(x0))))))))
a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
A(a(b(d(d(b(b(x0))))))) → B(b(a(a(c(c(x0))))))
A(a(d(d(b(b(x0)))))) → B(a(a(c(c(x0)))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
A(a(x1)) → B(b(x1))
B(b(d(d(b(b(x1)))))) → A(a(c(c(x1))))
A(a(x1)) → B(b(b(b(x1))))
A(a(d(d(b(b(x0)))))) → B(b(b(a(a(c(c(x0)))))))
A(a(d(d(b(b(x0)))))) → B(a(a(c(c(x0)))))
A(a(b(d(d(b(b(x0))))))) → B(b(a(a(c(c(x0))))))
A(a(x1)) → B(b(b(b(b(b(x1))))))
A(a(b(d(d(b(b(x0))))))) → B(b(b(b(a(a(c(c(x0))))))))
a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
A(a(b(d(d(b(b(x0))))))) → B(b(b(a(a(c(c(x0)))))))
A(a(d(d(b(b(x0)))))) → B(b(a(a(c(c(x0))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
A(a(x1)) → B(b(x1))
A(a(b(d(d(b(b(x0))))))) → B(b(b(a(a(c(c(x0)))))))
B(b(d(d(b(b(x1)))))) → A(a(c(c(x1))))
A(a(d(d(b(b(x0)))))) → B(b(b(a(a(c(c(x0)))))))
A(a(b(d(d(b(b(x0))))))) → B(b(a(a(c(c(x0))))))
A(a(d(d(b(b(x0)))))) → B(a(a(c(c(x0)))))
A(a(x1)) → B(b(b(b(b(b(x1))))))
A(a(d(d(b(b(x0)))))) → B(b(a(a(c(c(x0))))))
A(a(b(d(d(b(b(x0))))))) → B(b(b(b(a(a(c(c(x0))))))))
a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
A(a(d(d(b(b(x0)))))) → B(b(b(b(a(a(c(c(x0))))))))
A(a(b(d(d(b(b(x0))))))) → B(b(b(b(b(a(a(c(c(x0)))))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
A(a(b(d(d(b(b(x0))))))) → B(b(b(b(b(a(a(c(c(x0)))))))))
A(a(x1)) → B(b(x1))
A(a(b(d(d(b(b(x0))))))) → B(b(b(a(a(c(c(x0)))))))
B(b(d(d(b(b(x1)))))) → A(a(c(c(x1))))
A(a(d(d(b(b(x0)))))) → B(b(b(b(a(a(c(c(x0))))))))
A(a(d(d(b(b(x0)))))) → B(b(b(a(a(c(c(x0)))))))
A(a(d(d(b(b(x0)))))) → B(a(a(c(c(x0)))))
A(a(b(d(d(b(b(x0))))))) → B(b(a(a(c(c(x0))))))
A(a(b(d(d(b(b(x0))))))) → B(b(b(b(a(a(c(c(x0))))))))
A(a(d(d(b(b(x0)))))) → B(b(a(a(c(c(x0))))))
a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
A(a(b(d(d(b(b(x0))))))) → B(b(b(b(b(a(a(c(c(x0)))))))))
A(a(b(d(d(b(b(x0))))))) → B(b(b(a(a(c(c(x0)))))))
A(a(b(d(d(b(b(x0))))))) → B(b(a(a(c(c(x0))))))
A(a(b(d(d(b(b(x0))))))) → B(b(b(b(a(a(c(c(x0))))))))
Used ordering: Polynomial interpretation [25]:
A(a(x1)) → B(b(x1))
B(b(d(d(b(b(x1)))))) → A(a(c(c(x1))))
A(a(d(d(b(b(x0)))))) → B(b(b(b(a(a(c(c(x0))))))))
A(a(d(d(b(b(x0)))))) → B(b(b(a(a(c(c(x0)))))))
A(a(d(d(b(b(x0)))))) → B(a(a(c(c(x0)))))
A(a(d(d(b(b(x0)))))) → B(b(a(a(c(c(x0))))))
POL(A(x1)) = 4 + 14·x1
POL(B(x1)) = 6·x1
POL(a(x1)) = 1 + 2·x1
POL(b(x1)) = 3
POL(c(x1)) = 0
POL(d(x1)) = 0
c(c(x1)) → d(d(x1))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
a(a(d(d(x1)))) → d(d(b(b(x1))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
A(a(x1)) → B(b(x1))
B(b(d(d(b(b(x1)))))) → A(a(c(c(x1))))
A(a(d(d(b(b(x0)))))) → B(b(b(b(a(a(c(c(x0))))))))
A(a(d(d(b(b(x0)))))) → B(b(b(a(a(c(c(x0)))))))
A(a(d(d(b(b(x0)))))) → B(a(a(c(c(x0)))))
A(a(d(d(b(b(x0)))))) → B(b(a(a(c(c(x0))))))
a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
A.0(a.0(d.0(d.0(b.1(b.0(x0)))))) → B.0(a.0(a.0(c.0(c.0(x0)))))
B.1(b.0(d.0(d.1(b.0(b.1(x1)))))) → A.0(a.0(c.0(c.1(x1))))
A.0(a.0(d.0(d.0(b.1(b.0(x0)))))) → B.0(b.1(b.0(a.0(a.0(c.0(c.0(x0)))))))
A.0(a.0(d.0(d.0(b.1(b.0(x0)))))) → B.1(b.0(a.0(a.0(c.0(c.0(x0))))))
A.0(a.0(d.0(d.0(b.1(b.0(x0)))))) → B.1(b.0(b.1(b.0(a.0(a.0(c.0(c.0(x0))))))))
A.0(a.0(d.0(d.1(b.0(b.1(x0)))))) → B.1(b.0(a.0(a.0(c.0(c.1(x0))))))
A.0(a.0(d.0(d.1(b.0(b.1(x0)))))) → B.0(a.0(a.0(c.0(c.1(x0)))))
A.0(a.0(x1)) → B.1(b.0(x1))
B.1(b.0(d.0(d.0(b.1(b.0(x1)))))) → A.0(a.0(c.0(c.0(x1))))
A.0(a.0(d.0(d.1(b.0(b.1(x0)))))) → B.1(b.0(b.1(b.0(a.0(a.0(c.0(c.1(x0))))))))
A.1(a.1(x1)) → B.0(b.1(x1))
A.0(a.0(d.0(d.1(b.0(b.1(x0)))))) → B.0(b.1(b.0(a.0(a.0(c.0(c.1(x0)))))))
a.0(a.0(d.0(d.0(x1)))) → d.0(d.0(b.1(b.0(x1))))
a.0(a.0(d.0(d.1(x1)))) → d.0(d.1(b.0(b.1(x1))))
a.0(a.0(x1)) → b.1(b.0(b.1(b.0(b.1(b.0(x1))))))
b.1(b.0(d.0(d.1(b.0(b.1(x1)))))) → a.0(a.0(c.0(c.1(x1))))
b.1(b.0(d.0(d.0(b.1(b.0(x1)))))) → a.0(a.0(c.0(c.0(x1))))
c.0(c.1(x1)) → d.0(d.1(x1))
a.1(a.1(x1)) → b.0(b.1(b.0(b.1(b.0(b.1(x1))))))
c.0(c.0(x1)) → d.0(d.0(x1))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ SemLabProof2
A.0(a.0(d.0(d.0(b.1(b.0(x0)))))) → B.0(a.0(a.0(c.0(c.0(x0)))))
B.1(b.0(d.0(d.1(b.0(b.1(x1)))))) → A.0(a.0(c.0(c.1(x1))))
A.0(a.0(d.0(d.0(b.1(b.0(x0)))))) → B.0(b.1(b.0(a.0(a.0(c.0(c.0(x0)))))))
A.0(a.0(d.0(d.0(b.1(b.0(x0)))))) → B.1(b.0(a.0(a.0(c.0(c.0(x0))))))
A.0(a.0(d.0(d.0(b.1(b.0(x0)))))) → B.1(b.0(b.1(b.0(a.0(a.0(c.0(c.0(x0))))))))
A.0(a.0(d.0(d.1(b.0(b.1(x0)))))) → B.1(b.0(a.0(a.0(c.0(c.1(x0))))))
A.0(a.0(d.0(d.1(b.0(b.1(x0)))))) → B.0(a.0(a.0(c.0(c.1(x0)))))
A.0(a.0(x1)) → B.1(b.0(x1))
B.1(b.0(d.0(d.0(b.1(b.0(x1)))))) → A.0(a.0(c.0(c.0(x1))))
A.0(a.0(d.0(d.1(b.0(b.1(x0)))))) → B.1(b.0(b.1(b.0(a.0(a.0(c.0(c.1(x0))))))))
A.1(a.1(x1)) → B.0(b.1(x1))
A.0(a.0(d.0(d.1(b.0(b.1(x0)))))) → B.0(b.1(b.0(a.0(a.0(c.0(c.1(x0)))))))
a.0(a.0(d.0(d.0(x1)))) → d.0(d.0(b.1(b.0(x1))))
a.0(a.0(d.0(d.1(x1)))) → d.0(d.1(b.0(b.1(x1))))
a.0(a.0(x1)) → b.1(b.0(b.1(b.0(b.1(b.0(x1))))))
b.1(b.0(d.0(d.1(b.0(b.1(x1)))))) → a.0(a.0(c.0(c.1(x1))))
b.1(b.0(d.0(d.0(b.1(b.0(x1)))))) → a.0(a.0(c.0(c.0(x1))))
c.0(c.1(x1)) → d.0(d.1(x1))
a.1(a.1(x1)) → b.0(b.1(b.0(b.1(b.0(b.1(x1))))))
c.0(c.0(x1)) → d.0(d.0(x1))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ SemLabProof2
B.1(b.0(d.0(d.1(b.0(b.1(x1)))))) → A.0(a.0(c.0(c.1(x1))))
A.0(a.0(d.0(d.0(b.1(b.0(x0)))))) → B.1(b.0(a.0(a.0(c.0(c.0(x0))))))
A.0(a.0(d.0(d.0(b.1(b.0(x0)))))) → B.1(b.0(b.1(b.0(a.0(a.0(c.0(c.0(x0))))))))
A.0(a.0(d.0(d.1(b.0(b.1(x0)))))) → B.1(b.0(a.0(a.0(c.0(c.1(x0))))))
A.0(a.0(x1)) → B.1(b.0(x1))
B.1(b.0(d.0(d.0(b.1(b.0(x1)))))) → A.0(a.0(c.0(c.0(x1))))
A.0(a.0(d.0(d.1(b.0(b.1(x0)))))) → B.1(b.0(b.1(b.0(a.0(a.0(c.0(c.1(x0))))))))
a.0(a.0(d.0(d.0(x1)))) → d.0(d.0(b.1(b.0(x1))))
a.0(a.0(d.0(d.1(x1)))) → d.0(d.1(b.0(b.1(x1))))
a.0(a.0(x1)) → b.1(b.0(b.1(b.0(b.1(b.0(x1))))))
b.1(b.0(d.0(d.1(b.0(b.1(x1)))))) → a.0(a.0(c.0(c.1(x1))))
b.1(b.0(d.0(d.0(b.1(b.0(x1)))))) → a.0(a.0(c.0(c.0(x1))))
c.0(c.1(x1)) → d.0(d.1(x1))
a.1(a.1(x1)) → b.0(b.1(b.0(b.1(b.0(b.1(x1))))))
c.0(c.0(x1)) → d.0(d.0(x1))
POL(A.0(x1)) = x1
POL(B.1(x1)) = x1
POL(a.0(x1)) = x1
POL(b.0(x1)) = x1
POL(b.1(x1)) = x1
POL(c.0(x1)) = x1
POL(c.1(x1)) = x1
POL(d.0(x1)) = x1
POL(d.1(x1)) = x1
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ SemLabProof2
B.1(b.0(d.0(d.1(b.0(b.1(x1)))))) → A.0(a.0(c.0(c.1(x1))))
A.0(a.0(d.0(d.0(b.1(b.0(x0)))))) → B.1(b.0(a.0(a.0(c.0(c.0(x0))))))
A.0(a.0(d.0(d.0(b.1(b.0(x0)))))) → B.1(b.0(b.1(b.0(a.0(a.0(c.0(c.0(x0))))))))
A.0(a.0(d.0(d.1(b.0(b.1(x0)))))) → B.1(b.0(a.0(a.0(c.0(c.1(x0))))))
A.0(a.0(x1)) → B.1(b.0(x1))
B.1(b.0(d.0(d.0(b.1(b.0(x1)))))) → A.0(a.0(c.0(c.0(x1))))
A.0(a.0(d.0(d.1(b.0(b.1(x0)))))) → B.1(b.0(b.1(b.0(a.0(a.0(c.0(c.1(x0))))))))
c.0(c.1(x1)) → d.0(d.1(x1))
a.0(a.0(d.0(d.0(x1)))) → d.0(d.0(b.1(b.0(x1))))
a.0(a.0(d.0(d.1(x1)))) → d.0(d.1(b.0(b.1(x1))))
b.1(b.0(d.0(d.0(b.1(b.0(x1)))))) → a.0(a.0(c.0(c.0(x1))))
a.0(a.0(x1)) → b.1(b.0(b.1(b.0(b.1(b.0(x1))))))
b.1(b.0(d.0(d.1(b.0(b.1(x1)))))) → a.0(a.0(c.0(c.1(x1))))
c.0(c.0(x1)) → d.0(d.0(x1))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
A(a(x1)) → B(b(x1))
B(b(d(d(b(b(x1)))))) → A(a(c(c(x1))))
A(a(d(d(b(b(x0)))))) → B(b(b(b(a(a(c(c(x0))))))))
A(a(d(d(b(b(x0)))))) → B(b(a(a(c(c(x0))))))
a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
A(a(x1)) → B(b(x1))
B(b(d(d(b(b(x1)))))) → A(a(c(c(x1))))
A(a(d(d(b(b(x0)))))) → B(b(b(b(a(a(c(c(x0))))))))
A(a(d(d(b(b(x0)))))) → B(b(a(a(c(c(x0))))))
a(a(d(d(x1)))) → d(d(b(b(x1))))
a(a(x1)) → b(b(b(b(b(b(x1))))))
b(b(d(d(b(b(x1)))))) → a(a(c(c(x1))))
c(c(x1)) → d(d(x1))
A(a(x1)) → B(b(x1))
B(b(d(d(b(b(x1)))))) → A(a(c(c(x1))))
A(a(d(d(b(b(x0)))))) → B(b(b(b(a(a(c(c(x0))))))))
A(a(d(d(b(b(x0)))))) → B(b(a(a(c(c(x0))))))
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
a(A(x)) → b(B(x))
b(b(d(d(b(B(x)))))) → c(c(a(A(x))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(b(b(B(x))))))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(B(x))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
a(A(x)) → b(B(x))
b(b(d(d(b(B(x)))))) → c(c(a(A(x))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(b(b(B(x))))))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(B(x))))))
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
a(A(x)) → b(B(x))
b(b(d(d(b(B(x)))))) → c(c(a(A(x))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(b(b(B(x))))))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(B(x))))))
a(a(d(d(x)))) → d(d(b(b(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → a(a(c(c(x))))
c(c(x)) → d(d(x))
A(a(x)) → B(b(x))
B(b(d(d(b(b(x)))))) → A(a(c(c(x))))
A(a(d(d(b(b(x)))))) → B(b(b(b(a(a(c(c(x))))))))
A(a(d(d(b(b(x)))))) → B(b(a(a(c(c(x))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ DependencyPairsProof
a(a(d(d(x)))) → d(d(b(b(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → a(a(c(c(x))))
c(c(x)) → d(d(x))
A(a(x)) → B(b(x))
B(b(d(d(b(b(x)))))) → A(a(c(c(x))))
A(a(d(d(b(b(x)))))) → B(b(b(b(a(a(c(c(x))))))))
A(a(d(d(b(b(x)))))) → B(b(a(a(c(c(x))))))
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
a(A(x)) → b(B(x))
b(b(d(d(b(B(x)))))) → c(c(a(A(x))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(b(b(B(x))))))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(B(x))))))
a(a(d(d(x)))) → d(d(b(b(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → a(a(c(c(x))))
c(c(x)) → d(d(x))
A(a(x)) → B(b(x))
B(b(d(d(b(b(x)))))) → A(a(c(c(x))))
A(a(d(d(b(b(x)))))) → B(b(b(b(a(a(c(c(x))))))))
A(a(d(d(b(b(x)))))) → B(b(a(a(c(c(x))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ QTRS
↳ DependencyPairsProof
a(a(d(d(x)))) → d(d(b(b(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → a(a(c(c(x))))
c(c(x)) → d(d(x))
A(a(x)) → B(b(x))
B(b(d(d(b(b(x)))))) → A(a(c(c(x))))
A(a(d(d(b(b(x)))))) → B(b(b(b(a(a(c(c(x))))))))
A(a(d(d(b(b(x)))))) → B(b(a(a(c(c(x))))))
B1(b(d(d(a(A(x)))))) → B1(B(x))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(b(b(B(x))))))))
B1(b(d(d(b(b(x)))))) → C(a(a(x)))
B1(b(d(d(b(b(x)))))) → C(c(a(a(x))))
B1(b(d(d(a(A(x)))))) → C(a(a(b(b(b(B(x)))))))
B1(b(d(d(a(A(x)))))) → A1(b(B(x)))
B1(b(d(d(a(A(x)))))) → A1(a(b(B(x))))
B1(b(d(d(b(B(x)))))) → C(c(a(A(x))))
A1(a(x)) → B1(b(b(b(x))))
A1(a(x)) → B1(x)
C(c(x)) → D(d(x))
B1(b(d(d(a(A(x)))))) → B1(b(B(x)))
B1(b(d(d(a(A(x)))))) → A1(a(b(b(b(B(x))))))
D(d(a(a(x)))) → B1(b(d(d(x))))
D(d(a(a(x)))) → D(x)
B1(b(d(d(b(b(x)))))) → A1(x)
D(d(a(a(x)))) → D(d(x))
A1(a(x)) → B1(b(b(b(b(x)))))
A1(a(x)) → B1(b(b(x)))
B1(b(d(d(a(A(x)))))) → B1(b(b(B(x))))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(B(x))))))
B1(b(d(d(a(A(x)))))) → C(a(a(b(B(x)))))
C(c(x)) → D(x)
D(d(a(a(x)))) → B1(d(d(x)))
A1(a(x)) → B1(b(b(b(b(b(x))))))
B1(b(d(d(b(b(x)))))) → A1(a(x))
B1(b(d(d(b(B(x)))))) → C(a(A(x)))
B1(b(d(d(b(B(x)))))) → A1(A(x))
B1(b(d(d(a(A(x)))))) → A1(b(b(b(B(x)))))
A1(a(x)) → B1(b(x))
A1(A(x)) → B1(B(x))
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
a(A(x)) → b(B(x))
b(b(d(d(b(B(x)))))) → c(c(a(A(x))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(b(b(B(x))))))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(B(x))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
B1(b(d(d(a(A(x)))))) → B1(B(x))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(b(b(B(x))))))))
B1(b(d(d(b(b(x)))))) → C(a(a(x)))
B1(b(d(d(b(b(x)))))) → C(c(a(a(x))))
B1(b(d(d(a(A(x)))))) → C(a(a(b(b(b(B(x)))))))
B1(b(d(d(a(A(x)))))) → A1(b(B(x)))
B1(b(d(d(a(A(x)))))) → A1(a(b(B(x))))
B1(b(d(d(b(B(x)))))) → C(c(a(A(x))))
A1(a(x)) → B1(b(b(b(x))))
A1(a(x)) → B1(x)
C(c(x)) → D(d(x))
B1(b(d(d(a(A(x)))))) → B1(b(B(x)))
B1(b(d(d(a(A(x)))))) → A1(a(b(b(b(B(x))))))
D(d(a(a(x)))) → B1(b(d(d(x))))
D(d(a(a(x)))) → D(x)
B1(b(d(d(b(b(x)))))) → A1(x)
D(d(a(a(x)))) → D(d(x))
A1(a(x)) → B1(b(b(b(b(x)))))
A1(a(x)) → B1(b(b(x)))
B1(b(d(d(a(A(x)))))) → B1(b(b(B(x))))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(B(x))))))
B1(b(d(d(a(A(x)))))) → C(a(a(b(B(x)))))
C(c(x)) → D(x)
D(d(a(a(x)))) → B1(d(d(x)))
A1(a(x)) → B1(b(b(b(b(b(x))))))
B1(b(d(d(b(b(x)))))) → A1(a(x))
B1(b(d(d(b(B(x)))))) → C(a(A(x)))
B1(b(d(d(b(B(x)))))) → A1(A(x))
B1(b(d(d(a(A(x)))))) → A1(b(b(b(B(x)))))
A1(a(x)) → B1(b(x))
A1(A(x)) → B1(B(x))
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
a(A(x)) → b(B(x))
b(b(d(d(b(B(x)))))) → c(c(a(A(x))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(b(b(B(x))))))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(B(x))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
A1(a(x)) → B1(b(b(b(b(x)))))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(b(b(B(x))))))))
B1(b(d(d(b(b(x)))))) → C(a(a(x)))
A1(a(x)) → B1(b(b(x)))
B1(b(d(d(a(A(x)))))) → C(a(a(b(b(b(B(x)))))))
B1(b(d(d(b(b(x)))))) → C(c(a(a(x))))
B1(b(d(d(a(A(x)))))) → A1(a(b(B(x))))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(B(x))))))
B1(b(d(d(a(A(x)))))) → C(a(a(b(B(x)))))
C(c(x)) → D(x)
B1(b(d(d(b(B(x)))))) → C(c(a(A(x))))
A1(a(x)) → B1(b(b(b(x))))
D(d(a(a(x)))) → B1(d(d(x)))
A1(a(x)) → B1(x)
C(c(x)) → D(d(x))
B1(b(d(d(a(A(x)))))) → A1(a(b(b(b(B(x))))))
A1(a(x)) → B1(b(b(b(b(b(x))))))
D(d(a(a(x)))) → B1(b(d(d(x))))
B1(b(d(d(b(b(x)))))) → A1(a(x))
D(d(a(a(x)))) → D(x)
B1(b(d(d(b(b(x)))))) → A1(x)
D(d(a(a(x)))) → D(d(x))
B1(b(d(d(b(B(x)))))) → C(a(A(x)))
A1(a(x)) → B1(b(x))
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
a(A(x)) → b(B(x))
b(b(d(d(b(B(x)))))) → c(c(a(A(x))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(b(b(B(x))))))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(B(x))))))
B1(b(d(d(a(A(x)))))) → C(a(a(b(b(b(B(x)))))))
B1(b(d(d(a(A(x)))))) → A1(a(b(B(x))))
B1(b(d(d(a(A(x)))))) → C(a(a(b(B(x)))))
B1(b(d(d(a(A(x)))))) → A1(a(b(b(b(B(x))))))
B1(b(d(d(b(B(x)))))) → C(a(A(x)))
POL(A(x1)) = 1 + x1
POL(A1(x1)) = x1
POL(B(x1)) = 1 + x1
POL(B1(x1)) = x1
POL(C(x1)) = 2·x1
POL(D(x1)) = 2·x1
POL(a(x1)) = x1
POL(b(x1)) = x1
POL(c(x1)) = 2·x1
POL(d(x1)) = 2·x1
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
A1(a(x)) → B1(b(b(b(b(x)))))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(b(b(B(x))))))))
B1(b(d(d(b(b(x)))))) → C(a(a(x)))
A1(a(x)) → B1(b(b(x)))
B1(b(d(d(b(b(x)))))) → C(c(a(a(x))))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(B(x))))))
C(c(x)) → D(x)
B1(b(d(d(b(B(x)))))) → C(c(a(A(x))))
A1(a(x)) → B1(b(b(b(x))))
D(d(a(a(x)))) → B1(d(d(x)))
A1(a(x)) → B1(x)
C(c(x)) → D(d(x))
A1(a(x)) → B1(b(b(b(b(b(x))))))
B1(b(d(d(b(b(x)))))) → A1(a(x))
D(d(a(a(x)))) → B1(b(d(d(x))))
B1(b(d(d(b(b(x)))))) → A1(x)
D(d(a(a(x)))) → D(x)
D(d(a(a(x)))) → D(d(x))
A1(a(x)) → B1(b(x))
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
a(A(x)) → b(B(x))
b(b(d(d(b(B(x)))))) → c(c(a(A(x))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(b(b(B(x))))))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(B(x))))))
A1(a(x)) → B1(b(b(b(b(x)))))
B1(b(d(d(b(b(x)))))) → C(a(a(x)))
A1(a(x)) → B1(b(b(x)))
C(c(x)) → D(x)
A1(a(x)) → B1(b(b(b(x))))
A1(a(x)) → B1(x)
A1(a(x)) → B1(b(b(b(b(b(x))))))
B1(b(d(d(b(b(x)))))) → A1(a(x))
B1(b(d(d(b(b(x)))))) → A1(x)
D(d(a(a(x)))) → D(x)
A1(a(x)) → B1(b(x))
POL(A(x1)) = x1
POL(A1(x1)) = 1 + 2·x1
POL(B(x1)) = x1
POL(B1(x1)) = x1
POL(C(x1)) = 1 + 2·x1
POL(D(x1)) = 1 + 2·x1
POL(a(x1)) = x1
POL(b(x1)) = x1
POL(c(x1)) = 1 + 2·x1
POL(d(x1)) = 1 + 2·x1
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
D(d(a(a(x)))) → B1(d(d(x)))
C(c(x)) → D(d(x))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(b(b(B(x))))))))
D(d(a(a(x)))) → B1(b(d(d(x))))
D(d(a(a(x)))) → D(d(x))
B1(b(d(d(b(b(x)))))) → C(c(a(a(x))))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(B(x))))))
B1(b(d(d(b(B(x)))))) → C(c(a(A(x))))
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
a(A(x)) → b(B(x))
b(b(d(d(b(B(x)))))) → c(c(a(A(x))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(b(b(B(x))))))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(B(x))))))
D(d(a(a(d(a(a(x0))))))) → B1(d(b(b(d(d(x0))))))
D(d(a(a(a(a(x0)))))) → B1(b(b(d(d(x0)))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ ForwardInstantiation
C(c(x)) → D(d(x))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(b(b(B(x))))))))
D(d(a(a(x)))) → B1(b(d(d(x))))
D(d(a(a(d(a(a(x0))))))) → B1(d(b(b(d(d(x0))))))
B1(b(d(d(b(b(x)))))) → C(c(a(a(x))))
D(d(a(a(x)))) → D(d(x))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(B(x))))))
D(d(a(a(a(a(x0)))))) → B1(b(b(d(d(x0)))))
B1(b(d(d(b(B(x)))))) → C(c(a(A(x))))
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
a(A(x)) → b(B(x))
b(b(d(d(b(B(x)))))) → c(c(a(A(x))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(b(b(B(x))))))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(B(x))))))
C(c(a(a(a(a(y_0)))))) → D(d(a(a(a(a(y_0))))))
C(c(a(a(d(a(a(y_0))))))) → D(d(a(a(d(a(a(y_0)))))))
C(c(a(a(y_0)))) → D(d(a(a(y_0))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ DependencyGraphProof
C(c(a(a(d(a(a(y_0))))))) → D(d(a(a(d(a(a(y_0)))))))
C(c(a(a(a(a(y_0)))))) → D(d(a(a(a(a(y_0))))))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(b(b(B(x))))))))
D(d(a(a(x)))) → B1(b(d(d(x))))
C(c(a(a(y_0)))) → D(d(a(a(y_0))))
D(d(a(a(x)))) → D(d(x))
B1(b(d(d(b(b(x)))))) → C(c(a(a(x))))
D(d(a(a(d(a(a(x0))))))) → B1(d(b(b(d(d(x0))))))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(B(x))))))
D(d(a(a(a(a(x0)))))) → B1(b(b(d(d(x0)))))
B1(b(d(d(b(B(x)))))) → C(c(a(A(x))))
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
a(A(x)) → b(B(x))
b(b(d(d(b(B(x)))))) → c(c(a(A(x))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(b(b(B(x))))))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(B(x))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
C(c(a(a(d(a(a(y_0))))))) → D(d(a(a(d(a(a(y_0)))))))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(b(b(B(x))))))))
C(c(a(a(a(a(y_0)))))) → D(d(a(a(a(a(y_0))))))
D(d(a(a(x)))) → B1(b(d(d(x))))
C(c(a(a(y_0)))) → D(d(a(a(y_0))))
D(d(a(a(d(a(a(x0))))))) → B1(d(b(b(d(d(x0))))))
D(d(a(a(x)))) → D(d(x))
B1(b(d(d(b(b(x)))))) → C(c(a(a(x))))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(B(x))))))
D(d(a(a(a(a(x0)))))) → B1(b(b(d(d(x0)))))
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
a(A(x)) → b(B(x))
b(b(d(d(b(B(x)))))) → c(c(a(A(x))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(b(b(B(x))))))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(B(x))))))
D(d(a(a(a(a(y_0)))))) → D(d(a(a(y_0))))
D(d(a(a(a(a(a(a(y_0)))))))) → D(d(a(a(a(a(y_0))))))
D(d(a(a(a(a(d(a(a(y_0))))))))) → D(d(a(a(d(a(a(y_0)))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ SemLabProof2
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(b(b(B(x))))))))
D(d(a(a(a(a(y_0)))))) → D(d(a(a(y_0))))
C(c(a(a(y_0)))) → D(d(a(a(y_0))))
D(d(a(a(a(a(d(a(a(y_0))))))))) → D(d(a(a(d(a(a(y_0)))))))
D(d(a(a(d(a(a(x0))))))) → B1(d(b(b(d(d(x0))))))
B1(b(d(d(b(b(x)))))) → C(c(a(a(x))))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(B(x))))))
C(c(a(a(d(a(a(y_0))))))) → D(d(a(a(d(a(a(y_0)))))))
C(c(a(a(a(a(y_0)))))) → D(d(a(a(a(a(y_0))))))
D(d(a(a(x)))) → B1(b(d(d(x))))
D(d(a(a(a(a(a(a(y_0)))))))) → D(d(a(a(a(a(y_0))))))
D(d(a(a(a(a(x0)))))) → B1(b(b(d(d(x0)))))
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
a(A(x)) → b(B(x))
b(b(d(d(b(B(x)))))) → c(c(a(A(x))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(b(b(B(x))))))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(B(x))))))
D.0(d.0(a.0(a.0(x)))) → B1.1(b.0(d.0(d.0(x))))
D.0(d.1(a.1(a.1(a.1(a.1(y_0)))))) → D.0(d.1(a.1(a.1(y_0))))
B1.1(b.0(d.0(d.0(a.0(A.0(x)))))) → C.0(c.0(a.0(a.0(b.1(B.0(x))))))
C.0(c.0(a.0(a.0(a.0(a.0(y_0)))))) → D.0(d.0(a.0(a.0(a.0(a.0(y_0))))))
D.0(d.0(a.0(a.0(d.1(a.1(a.1(x0))))))) → B1.0(d.0(b.1(b.0(d.0(d.1(x0))))))
B1.1(b.0(d.0(d.0(a.0(A.1(x)))))) → C.0(c.0(a.0(a.0(b.1(b.0(b.1(B.1(x))))))))
B1.1(b.0(d.0(d.1(b.0(b.1(x)))))) → C.0(c.1(a.1(a.1(x))))
D.0(d.1(a.1(a.1(a.1(a.1(a.1(a.1(y_0)))))))) → D.0(d.1(a.1(a.1(a.1(a.1(y_0))))))
C.0(c.0(a.0(a.0(d.1(a.1(a.1(y_0))))))) → D.0(d.0(a.0(a.0(d.1(a.1(a.1(y_0)))))))
B1.1(b.0(d.0(d.0(a.0(A.0(x)))))) → C.0(c.0(a.0(a.0(b.1(b.0(b.1(B.0(x))))))))
C.0(c.1(a.1(a.1(a.1(a.1(y_0)))))) → D.0(d.1(a.1(a.1(a.1(a.1(y_0))))))
C.0(c.0(a.0(a.0(d.0(a.0(a.0(y_0))))))) → D.0(d.0(a.0(a.0(d.0(a.0(a.0(y_0)))))))
D.0(d.0(a.0(a.0(a.0(a.0(d.1(a.1(a.1(y_0))))))))) → D.0(d.0(a.0(a.0(d.1(a.1(a.1(y_0)))))))
D.0(d.0(a.0(a.0(a.0(a.0(a.0(a.0(y_0)))))))) → D.0(d.0(a.0(a.0(a.0(a.0(y_0))))))
D.0(d.1(a.1(a.1(x)))) → B1.1(b.0(d.0(d.1(x))))
B1.1(b.0(d.0(d.0(a.0(A.1(x)))))) → C.0(c.0(a.0(a.0(b.1(B.1(x))))))
D.0(d.0(a.0(a.0(a.0(a.0(y_0)))))) → D.0(d.0(a.0(a.0(y_0))))
D.0(d.0(a.0(a.0(a.0(a.0(d.0(a.0(a.0(y_0))))))))) → D.0(d.0(a.0(a.0(d.0(a.0(a.0(y_0)))))))
D.0(d.0(a.0(a.0(d.0(a.0(a.0(x0))))))) → B1.0(d.0(b.1(b.0(d.0(d.0(x0))))))
D.0(d.0(a.0(a.0(a.0(a.0(x0)))))) → B1.0(b.1(b.0(d.0(d.0(x0)))))
C.0(c.0(a.0(a.0(y_0)))) → D.0(d.0(a.0(a.0(y_0))))
C.0(c.1(a.1(a.1(y_0)))) → D.0(d.1(a.1(a.1(y_0))))
D.0(d.1(a.1(a.1(a.1(a.1(x0)))))) → B1.0(b.1(b.0(d.0(d.1(x0)))))
B1.1(b.0(d.0(d.0(b.1(b.0(x)))))) → C.0(c.0(a.0(a.0(x))))
a.0(A.1(x)) → b.1(B.1(x))
a.1(a.1(x)) → b.0(b.1(b.0(b.1(b.0(b.1(x))))))
a.0(A.0(x)) → b.1(B.0(x))
d.0(d.0(a.0(a.0(x)))) → b.1(b.0(d.0(d.0(x))))
d.0(d.1(a.1(a.1(x)))) → b.1(b.0(d.0(d.1(x))))
b.1(b.0(d.0(d.1(b.0(b.1(x)))))) → c.0(c.1(a.1(a.1(x))))
c.0(c.0(x)) → d.0(d.0(x))
b.1(b.0(d.0(d.0(b.1(B.0(x)))))) → c.0(c.0(a.0(A.0(x))))
b.1(b.0(d.0(d.0(a.0(A.0(x)))))) → c.0(c.0(a.0(a.0(b.1(b.0(b.1(B.0(x))))))))
b.1(b.0(d.0(d.0(b.1(b.0(x)))))) → c.0(c.0(a.0(a.0(x))))
b.1(b.0(d.0(d.0(a.0(A.1(x)))))) → c.0(c.0(a.0(a.0(b.1(B.1(x))))))
a.0(a.0(x)) → b.1(b.0(b.1(b.0(b.1(b.0(x))))))
b.1(b.0(d.0(d.0(a.0(A.0(x)))))) → c.0(c.0(a.0(a.0(b.1(B.0(x))))))
b.1(b.0(d.0(d.0(b.1(B.1(x)))))) → c.0(c.0(a.0(A.1(x))))
b.1(b.0(d.0(d.0(a.0(A.1(x)))))) → c.0(c.0(a.0(a.0(b.1(b.0(b.1(B.1(x))))))))
c.0(c.1(x)) → d.0(d.1(x))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ SemLabProof2
D.0(d.0(a.0(a.0(x)))) → B1.1(b.0(d.0(d.0(x))))
D.0(d.1(a.1(a.1(a.1(a.1(y_0)))))) → D.0(d.1(a.1(a.1(y_0))))
B1.1(b.0(d.0(d.0(a.0(A.0(x)))))) → C.0(c.0(a.0(a.0(b.1(B.0(x))))))
C.0(c.0(a.0(a.0(a.0(a.0(y_0)))))) → D.0(d.0(a.0(a.0(a.0(a.0(y_0))))))
D.0(d.0(a.0(a.0(d.1(a.1(a.1(x0))))))) → B1.0(d.0(b.1(b.0(d.0(d.1(x0))))))
B1.1(b.0(d.0(d.0(a.0(A.1(x)))))) → C.0(c.0(a.0(a.0(b.1(b.0(b.1(B.1(x))))))))
B1.1(b.0(d.0(d.1(b.0(b.1(x)))))) → C.0(c.1(a.1(a.1(x))))
D.0(d.1(a.1(a.1(a.1(a.1(a.1(a.1(y_0)))))))) → D.0(d.1(a.1(a.1(a.1(a.1(y_0))))))
C.0(c.0(a.0(a.0(d.1(a.1(a.1(y_0))))))) → D.0(d.0(a.0(a.0(d.1(a.1(a.1(y_0)))))))
B1.1(b.0(d.0(d.0(a.0(A.0(x)))))) → C.0(c.0(a.0(a.0(b.1(b.0(b.1(B.0(x))))))))
C.0(c.1(a.1(a.1(a.1(a.1(y_0)))))) → D.0(d.1(a.1(a.1(a.1(a.1(y_0))))))
C.0(c.0(a.0(a.0(d.0(a.0(a.0(y_0))))))) → D.0(d.0(a.0(a.0(d.0(a.0(a.0(y_0)))))))
D.0(d.0(a.0(a.0(a.0(a.0(d.1(a.1(a.1(y_0))))))))) → D.0(d.0(a.0(a.0(d.1(a.1(a.1(y_0)))))))
D.0(d.0(a.0(a.0(a.0(a.0(a.0(a.0(y_0)))))))) → D.0(d.0(a.0(a.0(a.0(a.0(y_0))))))
D.0(d.1(a.1(a.1(x)))) → B1.1(b.0(d.0(d.1(x))))
B1.1(b.0(d.0(d.0(a.0(A.1(x)))))) → C.0(c.0(a.0(a.0(b.1(B.1(x))))))
D.0(d.0(a.0(a.0(a.0(a.0(y_0)))))) → D.0(d.0(a.0(a.0(y_0))))
D.0(d.0(a.0(a.0(a.0(a.0(d.0(a.0(a.0(y_0))))))))) → D.0(d.0(a.0(a.0(d.0(a.0(a.0(y_0)))))))
D.0(d.0(a.0(a.0(d.0(a.0(a.0(x0))))))) → B1.0(d.0(b.1(b.0(d.0(d.0(x0))))))
D.0(d.0(a.0(a.0(a.0(a.0(x0)))))) → B1.0(b.1(b.0(d.0(d.0(x0)))))
C.0(c.0(a.0(a.0(y_0)))) → D.0(d.0(a.0(a.0(y_0))))
C.0(c.1(a.1(a.1(y_0)))) → D.0(d.1(a.1(a.1(y_0))))
D.0(d.1(a.1(a.1(a.1(a.1(x0)))))) → B1.0(b.1(b.0(d.0(d.1(x0)))))
B1.1(b.0(d.0(d.0(b.1(b.0(x)))))) → C.0(c.0(a.0(a.0(x))))
a.0(A.1(x)) → b.1(B.1(x))
a.1(a.1(x)) → b.0(b.1(b.0(b.1(b.0(b.1(x))))))
a.0(A.0(x)) → b.1(B.0(x))
d.0(d.0(a.0(a.0(x)))) → b.1(b.0(d.0(d.0(x))))
d.0(d.1(a.1(a.1(x)))) → b.1(b.0(d.0(d.1(x))))
b.1(b.0(d.0(d.1(b.0(b.1(x)))))) → c.0(c.1(a.1(a.1(x))))
c.0(c.0(x)) → d.0(d.0(x))
b.1(b.0(d.0(d.0(b.1(B.0(x)))))) → c.0(c.0(a.0(A.0(x))))
b.1(b.0(d.0(d.0(a.0(A.0(x)))))) → c.0(c.0(a.0(a.0(b.1(b.0(b.1(B.0(x))))))))
b.1(b.0(d.0(d.0(b.1(b.0(x)))))) → c.0(c.0(a.0(a.0(x))))
b.1(b.0(d.0(d.0(a.0(A.1(x)))))) → c.0(c.0(a.0(a.0(b.1(B.1(x))))))
a.0(a.0(x)) → b.1(b.0(b.1(b.0(b.1(b.0(x))))))
b.1(b.0(d.0(d.0(a.0(A.0(x)))))) → c.0(c.0(a.0(a.0(b.1(B.0(x))))))
b.1(b.0(d.0(d.0(b.1(B.1(x)))))) → c.0(c.0(a.0(A.1(x))))
b.1(b.0(d.0(d.0(a.0(A.1(x)))))) → c.0(c.0(a.0(a.0(b.1(b.0(b.1(B.1(x))))))))
c.0(c.1(x)) → d.0(d.1(x))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ SemLabProof2
D.0(d.1(a.1(a.1(a.1(a.1(y_0)))))) → D.0(d.1(a.1(a.1(y_0))))
D.0(d.0(a.0(a.0(x)))) → B1.1(b.0(d.0(d.0(x))))
B1.1(b.0(d.0(d.0(a.0(A.0(x)))))) → C.0(c.0(a.0(a.0(b.1(B.0(x))))))
C.0(c.0(a.0(a.0(a.0(a.0(y_0)))))) → D.0(d.0(a.0(a.0(a.0(a.0(y_0))))))
D.0(d.1(a.1(a.1(a.1(a.1(a.1(a.1(y_0)))))))) → D.0(d.1(a.1(a.1(a.1(a.1(y_0))))))
B1.1(b.0(d.0(d.0(a.0(A.1(x)))))) → C.0(c.0(a.0(a.0(b.1(b.0(b.1(B.1(x))))))))
B1.1(b.0(d.0(d.1(b.0(b.1(x)))))) → C.0(c.1(a.1(a.1(x))))
B1.1(b.0(d.0(d.0(a.0(A.0(x)))))) → C.0(c.0(a.0(a.0(b.1(b.0(b.1(B.0(x))))))))
C.0(c.0(a.0(a.0(d.1(a.1(a.1(y_0))))))) → D.0(d.0(a.0(a.0(d.1(a.1(a.1(y_0)))))))
C.0(c.1(a.1(a.1(a.1(a.1(y_0)))))) → D.0(d.1(a.1(a.1(a.1(a.1(y_0))))))
C.0(c.0(a.0(a.0(d.0(a.0(a.0(y_0))))))) → D.0(d.0(a.0(a.0(d.0(a.0(a.0(y_0)))))))
D.0(d.0(a.0(a.0(a.0(a.0(d.1(a.1(a.1(y_0))))))))) → D.0(d.0(a.0(a.0(d.1(a.1(a.1(y_0)))))))
D.0(d.0(a.0(a.0(a.0(a.0(a.0(a.0(y_0)))))))) → D.0(d.0(a.0(a.0(a.0(a.0(y_0))))))
D.0(d.1(a.1(a.1(x)))) → B1.1(b.0(d.0(d.1(x))))
B1.1(b.0(d.0(d.0(a.0(A.1(x)))))) → C.0(c.0(a.0(a.0(b.1(B.1(x))))))
D.0(d.0(a.0(a.0(a.0(a.0(y_0)))))) → D.0(d.0(a.0(a.0(y_0))))
D.0(d.0(a.0(a.0(a.0(a.0(d.0(a.0(a.0(y_0))))))))) → D.0(d.0(a.0(a.0(d.0(a.0(a.0(y_0)))))))
C.0(c.0(a.0(a.0(y_0)))) → D.0(d.0(a.0(a.0(y_0))))
C.0(c.1(a.1(a.1(y_0)))) → D.0(d.1(a.1(a.1(y_0))))
B1.1(b.0(d.0(d.0(b.1(b.0(x)))))) → C.0(c.0(a.0(a.0(x))))
a.0(A.1(x)) → b.1(B.1(x))
a.1(a.1(x)) → b.0(b.1(b.0(b.1(b.0(b.1(x))))))
a.0(A.0(x)) → b.1(B.0(x))
d.0(d.0(a.0(a.0(x)))) → b.1(b.0(d.0(d.0(x))))
d.0(d.1(a.1(a.1(x)))) → b.1(b.0(d.0(d.1(x))))
b.1(b.0(d.0(d.1(b.0(b.1(x)))))) → c.0(c.1(a.1(a.1(x))))
c.0(c.0(x)) → d.0(d.0(x))
b.1(b.0(d.0(d.0(b.1(B.0(x)))))) → c.0(c.0(a.0(A.0(x))))
b.1(b.0(d.0(d.0(a.0(A.0(x)))))) → c.0(c.0(a.0(a.0(b.1(b.0(b.1(B.0(x))))))))
b.1(b.0(d.0(d.0(b.1(b.0(x)))))) → c.0(c.0(a.0(a.0(x))))
b.1(b.0(d.0(d.0(a.0(A.1(x)))))) → c.0(c.0(a.0(a.0(b.1(B.1(x))))))
a.0(a.0(x)) → b.1(b.0(b.1(b.0(b.1(b.0(x))))))
b.1(b.0(d.0(d.0(a.0(A.0(x)))))) → c.0(c.0(a.0(a.0(b.1(B.0(x))))))
b.1(b.0(d.0(d.0(b.1(B.1(x)))))) → c.0(c.0(a.0(A.1(x))))
b.1(b.0(d.0(d.0(a.0(A.1(x)))))) → c.0(c.0(a.0(a.0(b.1(b.0(b.1(B.1(x))))))))
c.0(c.1(x)) → d.0(d.1(x))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ SemLabProof
↳ SemLabProof2
C(c(a(a(d(a(a(y_0))))))) → D(d(a(a(d(a(a(y_0)))))))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(b(b(B(x))))))))
C(c(a(a(a(a(y_0)))))) → D(d(a(a(a(a(y_0))))))
D(d(a(a(a(a(y_0)))))) → D(d(a(a(y_0))))
D(d(a(a(x)))) → B1(b(d(d(x))))
D(d(a(a(a(a(a(a(y_0)))))))) → D(d(a(a(a(a(y_0))))))
C(c(a(a(y_0)))) → D(d(a(a(y_0))))
D(d(a(a(a(a(d(a(a(y_0))))))))) → D(d(a(a(d(a(a(y_0)))))))
B1(b(d(d(b(b(x)))))) → C(c(a(a(x))))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(B(x))))))
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
a(A(x)) → b(B(x))
b(b(d(d(b(B(x)))))) → c(c(a(A(x))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(b(b(B(x))))))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(B(x))))))
C.0(c.0(a.0(a.1(d.0(a.0(a.0(y_0))))))) → D.1(d.0(a.0(a.1(d.0(a.0(a.0(y_0)))))))
D.1(d.0(a.0(a.0(x)))) → B1.0(b.0(d.1(d.0(x))))
B1.0(b.0(d.1(d.0(b.0(b.0(x)))))) → C.0(c.0(a.0(a.0(x))))
B1.0(b.0(d.1(d.0(a.0(A.0(x)))))) → C.0(c.0(a.0(a.0(b.0(B.0(x))))))
C.0(c.0(a.0(a.1(d.0(a.0(a.1(y_0))))))) → D.1(d.0(a.0(a.1(d.0(a.0(a.1(y_0)))))))
B1.0(b.0(d.1(d.0(b.0(b.1(x)))))) → C.0(c.0(a.0(a.1(x))))
D.1(d.0(a.0(a.0(a.0(a.1(d.0(a.0(a.1(y_0))))))))) → D.1(d.0(a.0(a.1(d.0(a.0(a.1(y_0)))))))
D.1(d.0(a.0(a.0(a.0(a.0(a.0(a.1(y_0)))))))) → D.1(d.0(a.0(a.0(a.0(a.1(y_0))))))
D.1(d.0(a.0(a.0(a.0(a.0(y_0)))))) → D.1(d.0(a.0(a.0(y_0))))
C.0(c.0(a.0(a.0(a.0(a.0(y_0)))))) → D.1(d.0(a.0(a.0(a.0(a.0(y_0))))))
B1.0(b.0(d.1(d.0(a.0(A.1(x)))))) → C.0(c.0(a.0(a.0(b.0(b.0(b.0(B.1(x))))))))
C.0(c.0(a.0(a.1(y_0)))) → D.1(d.0(a.0(a.1(y_0))))
D.1(d.0(a.0(a.0(a.0(a.1(y_0)))))) → D.1(d.0(a.0(a.1(y_0))))
D.1(d.0(a.0(a.0(a.0(a.1(d.0(a.0(a.0(y_0))))))))) → D.1(d.0(a.0(a.1(d.0(a.0(a.0(y_0)))))))
C.0(c.0(a.0(a.0(y_0)))) → D.1(d.0(a.0(a.0(y_0))))
D.1(d.0(a.0(a.1(x)))) → B1.0(b.1(d.0(d.1(x))))
D.1(d.0(a.0(a.0(a.0(a.0(a.0(a.0(y_0)))))))) → D.1(d.0(a.0(a.0(a.0(a.0(y_0))))))
C.0(c.0(a.0(a.0(a.0(a.1(y_0)))))) → D.1(d.0(a.0(a.0(a.0(a.1(y_0))))))
B1.0(b.0(d.1(d.0(a.0(A.0(x)))))) → C.0(c.0(a.0(a.0(b.0(b.0(b.0(B.0(x))))))))
B1.0(b.0(d.1(d.0(a.0(A.1(x)))))) → C.0(c.0(a.0(a.0(b.0(B.1(x))))))
a.0(a.1(x)) → b.0(b.0(b.0(b.0(b.0(b.1(x))))))
b.0(b.0(d.1(d.0(a.0(A.1(x)))))) → c.0(c.0(a.0(a.0(b.0(b.0(b.0(B.1(x))))))))
a.0(A.1(x)) → b.0(B.1(x))
c.0(c.0(x)) → d.1(d.0(x))
a.0(a.0(x)) → b.0(b.0(b.0(b.0(b.0(b.0(x))))))
d.1(d.0(a.0(a.1(x)))) → b.0(b.1(d.0(d.1(x))))
b.0(b.0(d.1(d.0(b.0(B.1(x)))))) → c.0(c.0(a.0(A.1(x))))
a.0(A.0(x)) → b.0(B.0(x))
b.0(b.0(d.1(d.0(b.0(b.0(x)))))) → c.0(c.0(a.0(a.0(x))))
b.0(b.0(d.1(d.0(a.0(A.1(x)))))) → c.0(c.0(a.0(a.0(b.0(B.1(x))))))
d.1(d.0(a.0(a.0(x)))) → b.0(b.0(d.1(d.0(x))))
b.0(b.0(d.1(d.0(b.0(b.1(x)))))) → c.0(c.0(a.0(a.1(x))))
b.0(b.0(d.1(d.0(a.0(A.0(x)))))) → c.0(c.0(a.0(a.0(b.0(b.0(b.0(B.0(x))))))))
b.0(b.0(d.1(d.0(b.0(B.0(x)))))) → c.0(c.0(a.0(A.0(x))))
b.0(b.0(d.1(d.0(a.0(A.0(x)))))) → c.0(c.0(a.0(a.0(b.0(B.0(x))))))
c.1(c.1(x)) → d.0(d.1(x))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ SemLabProof2
C.0(c.0(a.0(a.1(d.0(a.0(a.0(y_0))))))) → D.1(d.0(a.0(a.1(d.0(a.0(a.0(y_0)))))))
D.1(d.0(a.0(a.0(x)))) → B1.0(b.0(d.1(d.0(x))))
B1.0(b.0(d.1(d.0(b.0(b.0(x)))))) → C.0(c.0(a.0(a.0(x))))
B1.0(b.0(d.1(d.0(a.0(A.0(x)))))) → C.0(c.0(a.0(a.0(b.0(B.0(x))))))
C.0(c.0(a.0(a.1(d.0(a.0(a.1(y_0))))))) → D.1(d.0(a.0(a.1(d.0(a.0(a.1(y_0)))))))
B1.0(b.0(d.1(d.0(b.0(b.1(x)))))) → C.0(c.0(a.0(a.1(x))))
D.1(d.0(a.0(a.0(a.0(a.1(d.0(a.0(a.1(y_0))))))))) → D.1(d.0(a.0(a.1(d.0(a.0(a.1(y_0)))))))
D.1(d.0(a.0(a.0(a.0(a.0(a.0(a.1(y_0)))))))) → D.1(d.0(a.0(a.0(a.0(a.1(y_0))))))
D.1(d.0(a.0(a.0(a.0(a.0(y_0)))))) → D.1(d.0(a.0(a.0(y_0))))
C.0(c.0(a.0(a.0(a.0(a.0(y_0)))))) → D.1(d.0(a.0(a.0(a.0(a.0(y_0))))))
B1.0(b.0(d.1(d.0(a.0(A.1(x)))))) → C.0(c.0(a.0(a.0(b.0(b.0(b.0(B.1(x))))))))
C.0(c.0(a.0(a.1(y_0)))) → D.1(d.0(a.0(a.1(y_0))))
D.1(d.0(a.0(a.0(a.0(a.1(y_0)))))) → D.1(d.0(a.0(a.1(y_0))))
D.1(d.0(a.0(a.0(a.0(a.1(d.0(a.0(a.0(y_0))))))))) → D.1(d.0(a.0(a.1(d.0(a.0(a.0(y_0)))))))
C.0(c.0(a.0(a.0(y_0)))) → D.1(d.0(a.0(a.0(y_0))))
D.1(d.0(a.0(a.1(x)))) → B1.0(b.1(d.0(d.1(x))))
D.1(d.0(a.0(a.0(a.0(a.0(a.0(a.0(y_0)))))))) → D.1(d.0(a.0(a.0(a.0(a.0(y_0))))))
C.0(c.0(a.0(a.0(a.0(a.1(y_0)))))) → D.1(d.0(a.0(a.0(a.0(a.1(y_0))))))
B1.0(b.0(d.1(d.0(a.0(A.0(x)))))) → C.0(c.0(a.0(a.0(b.0(b.0(b.0(B.0(x))))))))
B1.0(b.0(d.1(d.0(a.0(A.1(x)))))) → C.0(c.0(a.0(a.0(b.0(B.1(x))))))
a.0(a.1(x)) → b.0(b.0(b.0(b.0(b.0(b.1(x))))))
b.0(b.0(d.1(d.0(a.0(A.1(x)))))) → c.0(c.0(a.0(a.0(b.0(b.0(b.0(B.1(x))))))))
a.0(A.1(x)) → b.0(B.1(x))
c.0(c.0(x)) → d.1(d.0(x))
a.0(a.0(x)) → b.0(b.0(b.0(b.0(b.0(b.0(x))))))
d.1(d.0(a.0(a.1(x)))) → b.0(b.1(d.0(d.1(x))))
b.0(b.0(d.1(d.0(b.0(B.1(x)))))) → c.0(c.0(a.0(A.1(x))))
a.0(A.0(x)) → b.0(B.0(x))
b.0(b.0(d.1(d.0(b.0(b.0(x)))))) → c.0(c.0(a.0(a.0(x))))
b.0(b.0(d.1(d.0(a.0(A.1(x)))))) → c.0(c.0(a.0(a.0(b.0(B.1(x))))))
d.1(d.0(a.0(a.0(x)))) → b.0(b.0(d.1(d.0(x))))
b.0(b.0(d.1(d.0(b.0(b.1(x)))))) → c.0(c.0(a.0(a.1(x))))
b.0(b.0(d.1(d.0(a.0(A.0(x)))))) → c.0(c.0(a.0(a.0(b.0(b.0(b.0(B.0(x))))))))
b.0(b.0(d.1(d.0(b.0(B.0(x)))))) → c.0(c.0(a.0(A.0(x))))
b.0(b.0(d.1(d.0(a.0(A.0(x)))))) → c.0(c.0(a.0(a.0(b.0(B.0(x))))))
c.1(c.1(x)) → d.0(d.1(x))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ SemLabProof2
D.1(d.0(a.0(a.0(a.0(a.0(y_0)))))) → D.1(d.0(a.0(a.0(y_0))))
B1.0(b.0(d.1(d.0(a.0(A.1(x)))))) → C.0(c.0(a.0(a.0(b.0(b.0(b.0(B.1(x))))))))
C.0(c.0(a.0(a.0(a.0(a.0(y_0)))))) → D.1(d.0(a.0(a.0(a.0(a.0(y_0))))))
D.1(d.0(a.0(a.0(x)))) → B1.0(b.0(d.1(d.0(x))))
B1.0(b.0(d.1(d.0(b.0(b.0(x)))))) → C.0(c.0(a.0(a.0(x))))
B1.0(b.0(d.1(d.0(a.0(A.0(x)))))) → C.0(c.0(a.0(a.0(b.0(B.0(x))))))
C.0(c.0(a.0(a.0(y_0)))) → D.1(d.0(a.0(a.0(y_0))))
D.1(d.0(a.0(a.0(a.0(a.0(a.0(a.0(y_0)))))))) → D.1(d.0(a.0(a.0(a.0(a.0(y_0))))))
B1.0(b.0(d.1(d.0(a.0(A.0(x)))))) → C.0(c.0(a.0(a.0(b.0(b.0(b.0(B.0(x))))))))
C.0(c.0(a.0(a.0(a.0(a.1(y_0)))))) → D.1(d.0(a.0(a.0(a.0(a.1(y_0))))))
B1.0(b.0(d.1(d.0(a.0(A.1(x)))))) → C.0(c.0(a.0(a.0(b.0(B.1(x))))))
D.1(d.0(a.0(a.0(a.0(a.0(a.0(a.1(y_0)))))))) → D.1(d.0(a.0(a.0(a.0(a.1(y_0))))))
a.0(a.1(x)) → b.0(b.0(b.0(b.0(b.0(b.1(x))))))
b.0(b.0(d.1(d.0(a.0(A.1(x)))))) → c.0(c.0(a.0(a.0(b.0(b.0(b.0(B.1(x))))))))
a.0(A.1(x)) → b.0(B.1(x))
c.0(c.0(x)) → d.1(d.0(x))
a.0(a.0(x)) → b.0(b.0(b.0(b.0(b.0(b.0(x))))))
d.1(d.0(a.0(a.1(x)))) → b.0(b.1(d.0(d.1(x))))
b.0(b.0(d.1(d.0(b.0(B.1(x)))))) → c.0(c.0(a.0(A.1(x))))
a.0(A.0(x)) → b.0(B.0(x))
b.0(b.0(d.1(d.0(b.0(b.0(x)))))) → c.0(c.0(a.0(a.0(x))))
b.0(b.0(d.1(d.0(a.0(A.1(x)))))) → c.0(c.0(a.0(a.0(b.0(B.1(x))))))
d.1(d.0(a.0(a.0(x)))) → b.0(b.0(d.1(d.0(x))))
b.0(b.0(d.1(d.0(b.0(b.1(x)))))) → c.0(c.0(a.0(a.1(x))))
b.0(b.0(d.1(d.0(a.0(A.0(x)))))) → c.0(c.0(a.0(a.0(b.0(b.0(b.0(B.0(x))))))))
b.0(b.0(d.1(d.0(b.0(B.0(x)))))) → c.0(c.0(a.0(A.0(x))))
b.0(b.0(d.1(d.0(a.0(A.0(x)))))) → c.0(c.0(a.0(a.0(b.0(B.0(x))))))
c.1(c.1(x)) → d.0(d.1(x))
POL(A.0(x1)) = x1
POL(A.1(x1)) = x1
POL(B.0(x1)) = x1
POL(B.1(x1)) = x1
POL(B1.0(x1)) = 1 + x1
POL(C.0(x1)) = 1 + x1
POL(D.1(x1)) = 1 + x1
POL(a.0(x1)) = x1
POL(a.1(x1)) = x1
POL(b.0(x1)) = x1
POL(b.1(x1)) = x1
POL(c.0(x1)) = x1
POL(d.0(x1)) = x1
POL(d.1(x1)) = x1
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ SemLabProof2
D.1(d.0(a.0(a.0(a.0(a.0(y_0)))))) → D.1(d.0(a.0(a.0(y_0))))
D.1(d.0(a.0(a.0(x)))) → B1.0(b.0(d.1(d.0(x))))
C.0(c.0(a.0(a.0(a.0(a.0(y_0)))))) → D.1(d.0(a.0(a.0(a.0(a.0(y_0))))))
B1.0(b.0(d.1(d.0(a.0(A.1(x)))))) → C.0(c.0(a.0(a.0(b.0(b.0(b.0(B.1(x))))))))
B1.0(b.0(d.1(d.0(b.0(b.0(x)))))) → C.0(c.0(a.0(a.0(x))))
C.0(c.0(a.0(a.0(y_0)))) → D.1(d.0(a.0(a.0(y_0))))
B1.0(b.0(d.1(d.0(a.0(A.0(x)))))) → C.0(c.0(a.0(a.0(b.0(B.0(x))))))
D.1(d.0(a.0(a.0(a.0(a.0(a.0(a.0(y_0)))))))) → D.1(d.0(a.0(a.0(a.0(a.0(y_0))))))
C.0(c.0(a.0(a.0(a.0(a.1(y_0)))))) → D.1(d.0(a.0(a.0(a.0(a.1(y_0))))))
B1.0(b.0(d.1(d.0(a.0(A.0(x)))))) → C.0(c.0(a.0(a.0(b.0(b.0(b.0(B.0(x))))))))
D.1(d.0(a.0(a.0(a.0(a.0(a.0(a.1(y_0)))))))) → D.1(d.0(a.0(a.0(a.0(a.1(y_0))))))
B1.0(b.0(d.1(d.0(a.0(A.1(x)))))) → C.0(c.0(a.0(a.0(b.0(B.1(x))))))
a.0(a.0(x)) → b.0(b.0(b.0(b.0(b.0(b.0(x))))))
b.0(b.0(d.1(d.0(b.0(b.1(x)))))) → c.0(c.0(a.0(a.1(x))))
b.0(b.0(d.1(d.0(a.0(A.1(x)))))) → c.0(c.0(a.0(a.0(b.0(b.0(b.0(B.1(x))))))))
b.0(b.0(d.1(d.0(a.0(A.0(x)))))) → c.0(c.0(a.0(a.0(b.0(b.0(b.0(B.0(x))))))))
c.0(c.0(x)) → d.1(d.0(x))
b.0(b.0(d.1(d.0(b.0(B.0(x)))))) → c.0(c.0(a.0(A.0(x))))
b.0(b.0(d.1(d.0(b.0(B.1(x)))))) → c.0(c.0(a.0(A.1(x))))
b.0(b.0(d.1(d.0(b.0(b.0(x)))))) → c.0(c.0(a.0(a.0(x))))
b.0(b.0(d.1(d.0(a.0(A.0(x)))))) → c.0(c.0(a.0(a.0(b.0(B.0(x))))))
d.1(d.0(a.0(a.0(x)))) → b.0(b.0(d.1(d.0(x))))
b.0(b.0(d.1(d.0(a.0(A.1(x)))))) → c.0(c.0(a.0(a.0(b.0(B.1(x))))))
d.1(d.0(a.0(a.1(x)))) → b.0(b.1(d.0(d.1(x))))
a.0(A.1(x)) → b.0(B.1(x))
a.0(a.1(x)) → b.0(b.0(b.0(b.0(b.0(b.1(x))))))
a.0(A.0(x)) → b.0(B.0(x))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(b(b(B(x))))))))
C(c(a(a(a(a(y_0)))))) → D(d(a(a(a(a(y_0))))))
D(d(a(a(a(a(y_0)))))) → D(d(a(a(y_0))))
D(d(a(a(x)))) → B1(b(d(d(x))))
D(d(a(a(a(a(a(a(y_0)))))))) → D(d(a(a(a(a(y_0))))))
C(c(a(a(y_0)))) → D(d(a(a(y_0))))
B1(b(d(d(b(b(x)))))) → C(c(a(a(x))))
B1(b(d(d(a(A(x)))))) → C(c(a(a(b(B(x))))))
d(d(a(a(x)))) → b(b(d(d(x))))
a(a(x)) → b(b(b(b(b(b(x))))))
b(b(d(d(b(b(x)))))) → c(c(a(a(x))))
c(c(x)) → d(d(x))
a(A(x)) → b(B(x))
b(b(d(d(b(B(x)))))) → c(c(a(A(x))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(b(b(B(x))))))))
b(b(d(d(a(A(x)))))) → c(c(a(a(b(B(x))))))